g:OCMon.
Linorder(|g|;x,y.(x  y)) & Cancel(|g|;|g|;*) & (z:|g|. monot(|g|;x,y.(x  y);w.z * w)) 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, OCMon
Definitions	True, T, x. t(x), x,y. t(x;y), t  T, , x f y, P & Q, x:A. B(x), Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y)), x(s), Mon, x(s1,s2), P  Q, SqStable(P), AbMon, OCMon
Lemmas	ocmon wf, decidable assert, sq stable from decidable, sq stable monot, sq stable all, sq stable cancel, monot wf, grp op wf, cancel wf, grp le wf, assert wf, grp car wf, linorder wf, sq stable and, sq stable connex, sq stable anti sym, sq stable trans, sq stable refl, connex wf, anti sym wf, trans wf, refl wf